Nuprl Lemma : randm_wf
11,40
postcript
pdf
i
,
j
:
. (
i
j
)
(randm(
i
;
j
)
int_seg(
i
; (
j
+ 1)))
latex
Definitions
,
t
T
,
x
:
A
.
B
(
x
)
,
A
B
,
a
<
b
,
x
:
A
B
(
x
)
,
P
Q
,
lelt(
i
;
j
;
k
)
,
#$n
,
n
+
m
,
P
Q
,
False
,
A
,
void
,
x
:
A
B
(
x
)
,
{
x
:
A
|
B
(
x
)}
,
int_seg(
i
;
j
)
,
randm(
i
;
j
)
Lemmas
le
wf
origin
i,j:
. (i 
j) 
(randm(i; j) 
int_seg(i; (j + 1))) i,j:. (i j) (randm(i; j) int_seg(i; (j + 1))) Tx:A. B(x) B
B(x)
Q Q
A
B(x)